Nuprl Lemma : es-E-interface_functionality
11,40
postcript
pdf
es
:ES,
X
,
Y
:AbsInterface(Top). (
e
:E. (
(
e
X
))
(
(
e
Y
)))
(E(
X
)
r E(
Y
))
latex
Definitions
E(
X
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
f
(
a
)
,
True
,
False
,
tt
,
ff
,
left
+
right
,
Unit
,
,
t
.1
,
P
Q
,
if
b
then
t
else
f
fi
,
AbsInterface(
A
)
,
x
:
A
B
(
x
)
,
ES
,
x
:
A
B
(
x
)
,
E
,
{
x
:
A
|
B
(
x
)}
,
Type
,
b
,
e
X
,
Top
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
es-is-interface
wf
,
assert
wf
,
bfalse
wf
,
btrue
wf
,
false
wf
,
true
wf
origin
es:ES, X, Y:AbsInterface(Top). (e:E. (
(e 
X)) 
((e Y))) (E(X) 
r E(Y)) es:ES, X, Y:AbsInterface(Top). (e:E. ((e X)) ((e Y))) (E(X) r E(Y)) 
Q
B(x)
B(x)b Xx:A. B(x) T